(0) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList(@x) → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort(@x) → quicksort(testList(#unit))
testQuicksort2(@x) → quicksort(testList(#unit))
The (relative) TRS S consists of the following rules:
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
Rewrite Strategy: INNERMOST
(1) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
testList/0
testQuicksort/0
testQuicksort2/0
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
#abs(#0) → #0
#abs(#neg(@x)) → #pos(@x)
#abs(#pos(@x)) → #pos(@x)
#abs(#s(@x)) → #pos(#s(@x))
#greater(@x, @y) → #ckgt(#compare(@x, @y))
append(@l, @ys) → append#1(@l, @ys)
append#1(::(@x, @xs), @ys) → ::(@x, append(@xs, @ys))
append#1(nil, @ys) → @ys
appendD(@l, @ys) → appendD#1(@l, @ys)
appendD#1(::(@x, @xs), @ys) → ::(@x, appendD(@xs, @ys))
appendD#1(nil, @ys) → @ys
quicksort(@l) → quicksort#1(@l)
quicksort#1(::(@z, @zs)) → quicksort#2(split(@z, @zs), @z)
quicksort#1(nil) → nil
quicksort#2(tuple#2(@xs, @ys), @z) → append(quicksort(@xs), ::(@z, quicksort(@ys)))
quicksortD(@l) → quicksortD#1(@l)
quicksortD#1(::(@z, @zs)) → quicksortD#2(splitD(@z, @zs), @z)
quicksortD#1(nil) → nil
quicksortD#2(tuple#2(@xs, @ys), @z) → appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))
split(@pivot, @l) → split#1(@l, @pivot)
split#1(::(@x, @xs), @pivot) → split#2(split(@pivot, @xs), @pivot, @x)
split#1(nil, @pivot) → tuple#2(nil, nil)
split#2(tuple#2(@ls, @rs), @pivot, @x) → split#3(#greater(@x, @pivot), @ls, @rs, @x)
split#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
split#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
splitD(@pivot, @l) → splitD#1(@l, @pivot)
splitD#1(::(@x, @xs), @pivot) → splitD#2(splitD(@pivot, @xs), @pivot, @x)
splitD#1(nil, @pivot) → tuple#2(nil, nil)
splitD#2(tuple#2(@ls, @rs), @pivot, @x) → splitD#3(#greater(@x, @pivot), @ls, @rs, @x)
splitD#3(#false, @ls, @rs, @x) → tuple#2(::(@x, @ls), @rs)
splitD#3(#true, @ls, @rs, @x) → tuple#2(@ls, ::(@x, @rs))
testList → ::(#abs(#0), ::(#abs(#pos(#s(#s(#s(#s(#0)))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#0))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#s(#0))))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#0))))))))), ::(#abs(#pos(#s(#0))), ::(#abs(#pos(#s(#s(#0)))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#s(#s(#0)))))))))), ::(#abs(#pos(#s(#s(#s(#s(#s(#s(#0)))))))), ::(#abs(#pos(#s(#s(#s(#0))))), nil))))))))))
testQuicksort → quicksort(testList)
testQuicksort2 → quicksort(testList)
The (relative) TRS S consists of the following rules:
#ckgt(#EQ) → #false
#ckgt(#GT) → #true
#ckgt(#LT) → #false
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)
Rewrite Strategy: INNERMOST
(3) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
append(::(@x7631_4, @xs7632_4), @ys) →+ ::(@x7631_4, append(@xs7632_4, @ys))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@xs7632_4 / ::(@x7631_4, @xs7632_4)].
The result substitution is [ ].
(4) BOUNDS(n^1, INF)